Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    prime(0)  → false
2:    prime(s(0))  → false
3:    prime(s(s(x)))  → prime1(s(s(x)),s(x))
4:    prime1(x,0)  → false
5:    prime1(x,s(0))  → true
6:    prime1(x,s(s(y)))  → and(not(divp(s(s(y)),x)),prime1(x,s(y)))
7:    divp(x,y)  → rem(x,y) = 0
There are 3 dependency pairs:
8:    PRIME(s(s(x)))  → PRIME1(s(s(x)),s(x))
9:    PRIME1(x,s(s(y)))  → DIVP(s(s(y)),x)
10:    PRIME1(x,s(s(y)))  → PRIME1(x,s(y))
The approximated dependency graph contains one SCC: {10}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 4, 2006